\begin{tabbing}
ecl{-}trans($x$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=ecl\_ind($x$;$k$,${\it test}$.ecl{-}base{-}tuple($k$;${\it test}$);$a$,$b$,$A$,$B$.combine{-}ecl{-}tuples($A$;$B$;$\lambda$$a$,$b$,$n$. 0$<_{2}$$n$\+
\\[0ex]$\wedge_{2}$ $a$($n$)
\\[0ex]$\vee_{2}$ $b$($n$) $\wedge_{2}$ $a$(0);$\lambda$$a$,$b$. $a$ $\vee_{2}$ $b$);$a$,$b$,$A$,$B$.combine{-}ecl{-}tuples2($A$;$B$;$\lambda$$x$,$a$,$b$,$n$. isl($x$)
\\[0ex]$\wedge_{2}$ (\=0$<_{2}$$n$ $\wedge_{2}$ if outl($x$)$\rightarrow$ $a$($n$) else $b$($n$) fi\+
\\[0ex]$\vee_{2}$ $n$=$_{2}$0 $\wedge_{2}$ $a$(0) $\wedge_{2}$ $b$(0));$\lambda$${\it ha}$,${\it hb}$,${\it eha}$,${\it ehb}$,$a$,$b$. $a$ $\wedge_{2}$ $\neg_{2}$${\it ehb}$
\-\\[0ex]$\vee_{2}$ $b$ $\wedge_{2}$ $\neg_{2}$${\it eha}$);$a$,$b$,$A$,$B$.combine{-}ecl{-}tuples2($A$;$B$;$\lambda$$x$,$a$,$b$,$n$. isl($x$)
\\[0ex]$\wedge_{2}$ if outl($x$)$\rightarrow$ $a$($n$) else $b$($n$) fi;$\lambda$${\it ha}$,${\it hb}$,${\it eha}$,${\it ehb}$,$a$,$b$. $a$ $\wedge_{2}$ $\neg_{2}$${\it hb}$ $\wedge_{2}$ $\neg_{2}$${\it ehb}$
\\[0ex]$\vee_{2}$ $b$ $\wedge_{2}$ $\neg_{2}$${\it ha}$ $\wedge_{2}$ $\neg_{2}$${\it eha}$);$a$,$A$.reset{-}ecl{-}tuple($A$);$a$,$m$,$A$.add{-}ecl{-}act($A$;$m$);$a$,$m$,$A$.ecl{-}add{-}throw($A$;$m$);$a$,$l$,$A$.ecl{-}add{-}catch($A$;$l$))
\-
\end{tabbing}